|
1: |
|
app'(app'(eq,0),0) |
→ true |
2: |
|
app'(app'(eq,0),app'(s,x)) |
→ false |
3: |
|
app'(app'(eq,app'(s,x)),0) |
→ false |
4: |
|
app'(app'(eq,app'(s,x)),app'(s,y)) |
→ app'(app'(eq,x),y) |
5: |
|
app'(app'(le,0),y) |
→ true |
6: |
|
app'(app'(le,app'(s,x)),0) |
→ false |
7: |
|
app'(app'(le,app'(s,x)),app'(s,y)) |
→ app'(app'(le,x),y) |
8: |
|
app'(app'(app,nil),y) |
→ y |
9: |
|
app'(app'(app,app'(app'(add,n),x)),y) |
→ app'(app'(add,n),app'(app'(app,x),y)) |
10: |
|
app'(min,app'(app'(add,n),nil)) |
→ n |
11: |
|
app'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x))) |
12: |
|
app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(min,app'(app'(add,n),x)) |
13: |
|
app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) |
→ app'(min,app'(app'(add,m),x)) |
14: |
|
app'(app'(rm,n),nil) |
→ nil |
15: |
|
app'(app'(rm,n),app'(app'(add,m),x)) |
→ app'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x)) |
16: |
|
app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ app'(app'(rm,n),x) |
17: |
|
app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ app'(app'(add,m),app'(app'(rm,n),x)) |
18: |
|
app'(app'(minsort,nil),nil) |
→ nil |
19: |
|
app'(app'(minsort,app'(app'(add,n),x)),y) |
→ app'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)),y) |
20: |
|
app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ app'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil)) |
21: |
|
app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ app'(app'(minsort,x),app'(app'(add,n),y)) |
|
There are 40 dependency pairs:
|
22: |
|
APP'(app'(eq,app'(s,x)),app'(s,y)) |
→ APP'(app'(eq,x),y) |
23: |
|
APP'(app'(eq,app'(s,x)),app'(s,y)) |
→ APP'(eq,x) |
24: |
|
APP'(app'(le,app'(s,x)),app'(s,y)) |
→ APP'(app'(le,x),y) |
25: |
|
APP'(app'(le,app'(s,x)),app'(s,y)) |
→ APP'(le,x) |
26: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),app'(app'(app,x),y)) |
27: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app'(app,x),y) |
28: |
|
APP'(app'(app,app'(app'(add,n),x)),y) |
→ APP'(app,x) |
29: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x))) |
30: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(if_min,app'(app'(le,n),m)) |
31: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(le,n),m) |
32: |
|
APP'(min,app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(le,n) |
33: |
|
APP'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(min,app'(app'(add,n),x)) |
34: |
|
APP'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(app'(add,n),x) |
35: |
|
APP'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) |
→ APP'(min,app'(app'(add,m),x)) |
36: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x)) |
37: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(if_rm,app'(app'(eq,n),m)),n) |
38: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(if_rm,app'(app'(eq,n),m)) |
39: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(app'(eq,n),m) |
40: |
|
APP'(app'(rm,n),app'(app'(add,m),x)) |
→ APP'(eq,n) |
41: |
|
APP'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ APP'(app'(rm,n),x) |
42: |
|
APP'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) |
→ APP'(rm,n) |
43: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(app'(add,m),app'(app'(rm,n),x)) |
44: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(app'(rm,n),x) |
45: |
|
APP'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) |
→ APP'(rm,n) |
46: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)),y) |
47: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)) |
48: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))) |
49: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(app'(eq,n),app'(min,app'(app'(add,n),x))) |
50: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(eq,n) |
51: |
|
APP'(app'(minsort,app'(app'(add,n),x)),y) |
→ APP'(min,app'(app'(add,n),x)) |
52: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil)) |
53: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil) |
54: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)) |
55: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(app,app'(app'(rm,n),x)),y) |
56: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app,app'(app'(rm,n),x)) |
57: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(app'(rm,n),x) |
58: |
|
APP'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) |
→ APP'(rm,n) |
59: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(app'(minsort,x),app'(app'(add,n),y)) |
60: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(minsort,x) |
61: |
|
APP'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) |
→ APP'(app'(add,n),y) |
|
The approximated dependency graph contains one SCC:
{22,24,27,29,31,33,35-37,39,41,44,46,47,49,51,53,55,57,59}.